/-
Copyright (c) 2018 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baanen
-/
import ring_theory.unique_factorization_domain
import ring_theory.localization.basic

/-!
# Localizations away from an element

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

## Main definitions

 * `is_localization.away (x : R) S` expresses that `S` is a localization away from `x`, as an
   abbreviation of `is_localization (submonoid.powers x) S`
 * `exists_reduced_fraction (hb : b ≠ 0)` produces a reduced fraction of the form `b = a * x^n` for
   some `n : ℤ` and some `a : R` that is not divisible by `x`.

## Implementation notes

See `src/ring_theory/localization/basic.lean` for a design overview.

## Tags
localization, ring localization, commutative ring localization, characteristic predicate,
commutative ring, field of fractions
-/

section comm_semiring

variables {R : Type*} [comm_semiring R] (M : submonoid R) {S : Type*} [comm_semiring S]
variables [algebra R S] {P : Type*} [comm_semiring P]

namespace is_localization

section away

variables (x : R)

/-- Given `x : R`, the typeclass `is_localization.away x S` states that `S` is
isomorphic to the localization of `R` at the submonoid generated by `x`. -/
abbreviation away (S : Type*) [comm_semiring S] [algebra R S] :=
is_localization (submonoid.powers x) S

namespace away

variables [is_localization.away x S]

/-- Given `x : R` and a localization map `F : R →+* S` away from `x`, `inv_self` is `(F x)⁻¹`. -/
noncomputable def inv_self : S :=
mk' S (1 : R) ⟨x, submonoid.mem_powers _⟩

@[simp] lemma mul_inv_self : algebra_map R S x * inv_self x = 1 :=
by { convert is_localization.mk'_mul_mk'_eq_one _ 1, symmetry, apply is_localization.mk'_one }

variables {g : R →+* P}

/-- Given `x : R`, a localization map `F : R →+* S` away from `x`, and a map of `comm_semiring`s
`g : R →+* P` such that `g x` is invertible, the homomorphism induced from `S` to `P` sending
`z : S` to `g y * (g x)⁻ⁿ`, where `y : R, n : ℕ` are such that `z = F y * (F x)⁻ⁿ`. -/
noncomputable def lift (hg : is_unit (g x)) : S →+* P :=
is_localization.lift $ λ (y : submonoid.powers x), show is_unit (g y.1),
begin
  obtain ⟨n, hn⟩ := y.2,
  rw [←hn, g.map_pow],
  exact is_unit.map (pow_monoid_hom n : P →* P) hg,
end

@[simp] lemma away_map.lift_eq (hg : is_unit (g x)) (a : R) :
  lift x hg ((algebra_map R S) a) = g a := lift_eq _ _

@[simp] lemma away_map.lift_comp (hg : is_unit (g x)) :
  (lift x hg).comp (algebra_map R S) = g := lift_comp _

/-- Given `x y : R` and localizations `S`, `P` away from `x` and `x * y`
respectively, the homomorphism induced from `S` to `P`. -/
noncomputable def away_to_away_right (y : R) [algebra R P] [is_localization.away (x * y) P] :
  S →+* P :=
lift x $ show is_unit ((algebra_map R P) x), from
is_unit_of_mul_eq_one ((algebra_map R P) x) (mk' P y ⟨x * y, submonoid.mem_powers _⟩) $
by rw [mul_mk'_eq_mk'_of_mul, mk'_self]

variables (S) (Q : Type*) [comm_semiring Q] [algebra P Q]

/-- Given a map `f : R →+* S` and an element `r : R`, we may construct a map `Rᵣ →+* Sᵣ`. -/
noncomputable
def map (f : R →+* P) (r : R) [is_localization.away r S]
  [is_localization.away (f r) Q] : S →+* Q :=
is_localization.map Q f
  (show submonoid.powers r ≤ (submonoid.powers (f r)).comap f,
    by { rintros x ⟨n, rfl⟩, use n, simp })

end away

end away

variables [is_localization M S]

section at_units
variables (R) (S) (M)

/-- The localization at a module of units is isomorphic to the ring -/
noncomputable
def at_units (H : ∀ x : M, is_unit (x : R)) : R ≃ₐ[R] S :=
begin
  refine alg_equiv.of_bijective (algebra.of_id R S) ⟨_, _⟩,
  { intros x y hxy,
    obtain ⟨c, eq⟩ := (is_localization.eq_iff_exists M S).mp hxy,
    obtain ⟨u, hu⟩ := H c,
    rwa [← hu, units.mul_right_inj] at eq },
  { intros y,
    obtain ⟨⟨x, s⟩, eq⟩ := is_localization.surj M y,
    obtain ⟨u, hu⟩ := H s,
    use x * u.inv,
    dsimp only [algebra.of_id, ring_hom.to_fun_eq_coe, alg_hom.coe_mk],
    rw [ring_hom.map_mul, ← eq, ← hu, mul_assoc, ← ring_hom.map_mul],
    simp }
end

/-- The localization away from a unit is isomorphic to the ring -/
noncomputable
def at_unit (x : R) (e : is_unit x) [is_localization.away x S] : R ≃ₐ[R] S :=
begin
  apply at_units R (submonoid.powers x),
  rintros ⟨xn, n, hxn⟩,
  obtain ⟨u, hu⟩ := e,
  rw is_unit_iff_exists_inv,
  use u.inv ^ n,
  simp[← hxn, ← hu, ← mul_pow]
end

/-- The localization at one is isomorphic to the ring. -/
noncomputable
def at_one [is_localization.away (1 : R) S] : R ≃ₐ[R] S :=
@at_unit R _ S _ _ (1 : R) is_unit_one _

lemma away_of_is_unit_of_bijective {R : Type*} (S : Type*) [comm_ring R] [comm_ring S]
  [algebra R S] {r : R} (hr : is_unit r) (H : function.bijective (algebra_map R S)) :
  is_localization.away r S :=
{ map_units := by { rintros ⟨_, n, rfl⟩, exact (algebra_map R S).is_unit_map (hr.pow _) },
  surj := λ z, by { obtain ⟨z', rfl⟩ := H.2 z, exact ⟨⟨z', 1⟩, by simp⟩ },
  eq_iff_exists := λ x y, begin
    erw H.1.eq_iff,
    split,
    { rintro rfl, exact ⟨1, rfl⟩ },
    { rintro ⟨⟨_, n, rfl⟩, e⟩, exact (hr.pow _).mul_right_inj.mp e }
  end }

end at_units

end is_localization

namespace localization

open is_localization

variables {M}

/-- Given a map `f : R →+* S` and an element `r : R`, such that `f r` is invertible,
  we may construct a map `Rᵣ →+* S`. -/
noncomputable
abbreviation away_lift (f : R →+* P) (r : R) (hr : is_unit (f r)) :
  localization.away r →+* P :=
is_localization.away.lift r hr

/-- Given a map `f : R →+* S` and an element `r : R`, we may construct a map `Rᵣ →+* Sᵣ`. -/
noncomputable
abbreviation away_map (f : R →+* P) (r : R) :
  localization.away r →+* localization.away (f r) :=
is_localization.away.map _ _ f r

end localization

end comm_semiring

open localization

variables {R : Type*} [comm_ring R]

section num_denom

open unique_factorization_monoid is_localization

variable (x : R)

variables (B : Type*) [comm_ring B] [algebra R B] [is_localization.away x B]

/-- `self_zpow x (m : ℤ)` is `x ^ m` as an element of the localization away from `x`. -/
noncomputable def self_zpow (m : ℤ) : B :=
if hm : 0 ≤ m
then algebra_map _ _ x ^ m.nat_abs
else mk' _ (1 : R) (submonoid.pow x m.nat_abs)

lemma self_zpow_of_nonneg {n : ℤ} (hn : 0 ≤ n) : self_zpow x B n =
  algebra_map R B x ^ n.nat_abs :=
dif_pos hn

@[simp] lemma self_zpow_coe_nat (d : ℕ) : self_zpow x B d = (algebra_map R B x)^d :=
self_zpow_of_nonneg _ _ (int.coe_nat_nonneg d)

@[simp] lemma self_zpow_zero : self_zpow x B 0 = 1 :=
by simp [self_zpow_of_nonneg _ _ le_rfl]

lemma self_zpow_of_neg {n : ℤ} (hn : n < 0) :
  self_zpow x B n = mk' _ (1 : R) (submonoid.pow x n.nat_abs) :=
dif_neg hn.not_le

lemma self_zpow_of_nonpos {n : ℤ} (hn : n ≤ 0) :
  self_zpow x B n = mk' _ (1 : R) (submonoid.pow x n.nat_abs) :=
begin
  by_cases hn0 : n = 0,
  { simp [hn0, self_zpow_zero, submonoid.pow_apply] },
  { simp [self_zpow_of_neg _ _ (lt_of_le_of_ne hn hn0)] }
end

@[simp] lemma self_zpow_neg_coe_nat (d : ℕ) :
  self_zpow x B (-d) = mk' _ (1 : R) (submonoid.pow x d) :=
by simp [self_zpow_of_nonpos _ _ (neg_nonpos.mpr (int.coe_nat_nonneg d))]

@[simp] lemma self_zpow_sub_cast_nat {n m : ℕ} :
  self_zpow x B (n - m) = mk' _ (x ^ n) (submonoid.pow x m) :=
begin
  by_cases h : m ≤ n,
  { rw [is_localization.eq_mk'_iff_mul_eq, submonoid.pow_apply, subtype.coe_mk,
        ← int.coe_nat_sub h, self_zpow_coe_nat, ← map_pow, ← map_mul, ← pow_add,
        nat.sub_add_cancel h] },
  { rw [← neg_sub, ← int.coe_nat_sub (le_of_not_le h), self_zpow_neg_coe_nat,
        is_localization.mk'_eq_iff_eq],
    simp [submonoid.pow_apply, ← pow_add, nat.sub_add_cancel (le_of_not_le h)] }
end

@[simp] lemma self_zpow_add {n m : ℤ} :
  self_zpow x B (n + m) = self_zpow x B n * self_zpow x B m :=
begin
  cases le_or_lt 0 n with hn hn; cases le_or_lt 0 m with hm hm,
  { rw [self_zpow_of_nonneg _ _ hn, self_zpow_of_nonneg _ _ hm,
        self_zpow_of_nonneg _ _ (add_nonneg hn hm), int.nat_abs_add_nonneg hn hm, pow_add] },
  { have : n + m = n.nat_abs - m.nat_abs,
    { rw [int.nat_abs_of_nonneg hn, int.of_nat_nat_abs_of_nonpos hm.le, sub_neg_eq_add] },
    rw [self_zpow_of_nonneg _ _ hn, self_zpow_of_neg _ _ hm,
        this, self_zpow_sub_cast_nat, is_localization.mk'_eq_mul_mk'_one, map_pow] },
  { have : n + m = m.nat_abs - n.nat_abs,
    { rw [int.nat_abs_of_nonneg hm, int.of_nat_nat_abs_of_nonpos hn.le, sub_neg_eq_add, add_comm] },
    rw [self_zpow_of_nonneg _ _ hm, self_zpow_of_neg _ _ hn,
        this, self_zpow_sub_cast_nat, is_localization.mk'_eq_mul_mk'_one, map_pow, mul_comm] },
  { rw [self_zpow_of_neg _ _ hn, self_zpow_of_neg _ _ hm, self_zpow_of_neg _ _ (add_neg hn hm),
        int.nat_abs_add_neg hn hm, ← mk'_mul, one_mul],
    congr,
    ext,
    simp [pow_add] },
end

lemma self_zpow_mul_neg (d : ℤ) : self_zpow x B d * self_zpow x B (-d) = 1 :=
begin
  by_cases hd : d ≤ 0,
  { erw [self_zpow_of_nonpos x B hd, self_zpow_of_nonneg, ← map_pow, int.nat_abs_neg,
      is_localization.mk'_spec, map_one],
    apply nonneg_of_neg_nonpos,
    rwa [neg_neg]},
  { erw [self_zpow_of_nonneg x B (le_of_not_le hd), self_zpow_of_nonpos, ← map_pow, int.nat_abs_neg,
     @is_localization.mk'_spec' R _ (submonoid.powers x) B _ _ _ 1 (submonoid.pow x d.nat_abs),
      map_one],
    refine nonpos_of_neg_nonneg (le_of_lt _),
    rwa [neg_neg, ← not_le] },
end

lemma self_zpow_neg_mul (d : ℤ) : self_zpow x B (-d) * self_zpow x B d = 1 :=
by rw [mul_comm, self_zpow_mul_neg x B d]


lemma self_zpow_pow_sub (a : R) (b : B) (m d : ℤ) :
  (self_zpow x B (m - d)) * mk' B a (1 : submonoid.powers x) = b ↔
  (self_zpow x B m) * mk' B a (1 : submonoid.powers x) = (self_zpow x B d) * b :=
begin
  rw [sub_eq_add_neg, self_zpow_add, mul_assoc, mul_comm _ (mk' B a 1), ← mul_assoc],
  split,
  { intro h,
    have := congr_arg (λ s : B, s * self_zpow x B d) h,
    simp only at this,
    rwa [mul_assoc, mul_assoc, self_zpow_neg_mul, mul_one, mul_comm b _] at this},
  { intro h,
    have := congr_arg (λ s : B, s * self_zpow x B (-d)) h,
    simp only at this,
    rwa [mul_comm _ b, mul_assoc b _ _, self_zpow_mul_neg, mul_one] at this}
end


variables [is_domain R] [normalization_monoid R] [unique_factorization_monoid R]


theorem exists_reduced_fraction' {b : B} (hb : b ≠ 0) (hx : irreducible x) :
  ∃ (a : R) (n : ℤ), ¬ x ∣ a ∧
    self_zpow x B n * algebra_map R B a = b :=
begin
  classical,
  obtain ⟨⟨a₀, y⟩, H⟩ := surj (submonoid.powers x) b,
  obtain ⟨d, hy⟩ := (submonoid.mem_powers_iff y.1 x).mp y.2,
  have ha₀ : a₀ ≠ 0,
  { haveI := @is_domain_of_le_non_zero_divisors B _ R _ _ _ (submonoid.powers x) _
      (powers_le_non_zero_divisors_of_no_zero_divisors hx.ne_zero),
    simp only [map_zero, ← subtype.val_eq_coe, ← hy, map_pow] at H,
    apply ((injective_iff_map_eq_zero' (algebra_map R B)).mp _ a₀).mpr.mt,
    rw ← H,
    apply mul_ne_zero hb (pow_ne_zero _ _),
    exact is_localization.to_map_ne_zero_of_mem_non_zero_divisors B
      (powers_le_non_zero_divisors_of_no_zero_divisors (hx.ne_zero))
      (mem_non_zero_divisors_iff_ne_zero.mpr hx.ne_zero),
    exact is_localization.injective B (powers_le_non_zero_divisors_of_no_zero_divisors
      (hx.ne_zero)) },
  simp only [← subtype.val_eq_coe, ← hy] at H,
  obtain ⟨m, a, hyp1, hyp2⟩ := max_power_factor ha₀ hx,
  refine ⟨a, m-d, _⟩,
  rw [← mk'_one B, self_zpow_pow_sub, self_zpow_coe_nat, self_zpow_coe_nat, ← map_pow _ _ d,
    mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m],
  exact ⟨hyp1, (congr_arg _ (is_localization.mk'_one _ _))⟩,
end

end num_denom
